/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */

package expression;

import core.Node;
import core.UnsatException;
import domain.Domain;

/**
 *
 * @author ddoose
 */
public class Not extends IntExpr {
    
    public Not(Node n) {
        super(n);
        current = Domain.BOOLEAN;
        target = Domain.BOOLEAN;
    }
    
    public Not(Node c, IntExpr p) {
        super(c, p);
        current = Domain.BOOLEAN;
        target = Domain.BOOLEAN;
    }
    
    public boolean same(IntExpr i) {
        return (i instanceof Not) && sameParameters(i);
    }

    public void eval() throws UnsatException {
        Domain p = node.getIntExpr(getParameters().get(0)).current;
        
        // FALSE
        if (p.isFalse()) {
            reduceCurrent(Domain.FALSE);
        }
        // TRUE
        else if (p.isTrue()) {
            reduceCurrent(Domain.TRUE);
        }
    }

    public void propagate() throws UnsatException {
        IntExpr p = node.getIntExpr(getParameters().get(0));

        if (target.isTrue()) {
            p.reduceTarget(Domain.FALSE);
        }
        else if (target.isFalse()) {
            p.reduceTarget(Domain.TRUE);
        }
    }
    
    public boolean reduce() {
        // FALSE
        if (current.isFalse()) {
            Value v = node.createValue(0);
            node.replaceIntExpr(id, v.getId());
            return true;
        }
        // TRUE
        if (current.isTrue()) {
            Value v = node.createValue(1);
            node.replaceIntExpr(id, v.getId());
            return true;
        }
        return false;
    }
    
    public Not clone(Node n) {
        Not not = new Not(n);
        not.clone(this);
        return not;
    }
    
    public String toString() {
        return "(not " + node.getIntExpr(getParameters().get(0)) + ")";
    }

    public String pretty() {
        return id + "\t" + current + "\t" + target + "\t" + toString();
    }
}
